My delay in approving this is because of buchiFamily_saturation. I have looked at this off and on and could make some incremental grind improvements, but I don't have the subject expertise here. Is there anything that can be split off in separate lemmas? The existential from mem_buchiFamily seems to make this awkward, but is there any way this could be reworked more cleanly?

We can work on this after I get back from my trip on March 12. I don't have my laptop with me now.

@chenson2018 Could you elaborate on your last comment? I'm not sure I understand it. buchiFamly is an indexed family of omega-regular languages, where each index is a pair of equivalence classes of na.BuchiCongruence. The theorem men_buchiFamily merely relates a member of such a language with the two equivalence classes of its index. I don't think the proof of buchiFamily_saturation can be simplified much. If you still have the survey article by W. Thomas I sent you, this proof is essentially a formalization of the proof of part (a) of lemma 2.2 on page 140.

@ctchou Let me take another look and at least add the cleanups to grind usage I'd done locally. My question was essentially if you can rephrase the existentials to be "constructive" so it'd be easier to extract some smaller lemmas.

I don't think that's possible. In essence, here we are starting with something like x ∈ U * V^ω. Both the concatenation operation * and the omega power operation ^ω are essentially nondeterministic operations. For example, x ∈ U * V^ω merely says that x is the concatenation of some finite sequence from U followed by some infinite sequence from V^ω. We have no other information and no way to avoid the existential quantifiers.

@ctchou Please see my last commit and let me know what you think. My aim here was to as much as possible organize things into as few calls to grind as possible and to keep the number of available hypothesis minimized at each area of the proof.

(There is one particularly problematic call to grind I will point out separately.)

@chenson2018 It's a pleasure working with you.